(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const _8-0 (_ BitVec 8))
(assert v12)
(declare-const v15 Bool)
(assert v9)
(assert v9)
(assert v4)
(declare-const v16 Bool)
(declare-const _15-0 (_ BitVec 15))
(assert v8)
(assert (distinct v1 (= v4 v1 v9 v0 v6 v2 v8 v15)))
(assert (= v13 v9 v14))
(declare-const v17 Bool)
(assert (exists ((q0 (_ BitVec 15)) (q1 (_ BitVec 8)) (q2 Bool)) (xor (= (bvor _8-0 _8-0) q1 (bvor _8-0 _8-0) (bvor _8-0 _8-0) q1) (= _15-0 _15-0 q0 _15-0 q0) (xor v12 q2 q2 q2 (distinct #x331 #x331 #x331 #x331) v11 v4 v2 q2))))
(assert (=> v14 (= v4 v1 v9 v0 v6 v2 v8 v15)))
(assert v3)
(declare-const v18 Bool)
(declare-const v19 Bool)
(assert (xor v8 v6 (distinct (_ bv321 9) (_ bv321 9)) v7))
(declare-const v20 Bool)
(declare-const _3-0 (_ BitVec 3))
(assert v7)
(assert v14)
(check-sat)
